Nuprl Lemma : ma-single-rframe_wf
11,40
postcript
pdf
x
:Id,
L
:(Knd List). only members of
L
read
x
MsgA
latex
Definitions
t
T
,
Id
,
Knd
,
type
List
,
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
x
:
v
,
IdLnk
,
,
x
:
A
B
(
x
)
,
Void
,
Type
,
Top
,
x
:
A
B
(
x
)
,
State(
ds
)
,
,
mk-ma
,
only members of
L
read
x
,
MsgA
Lemmas
mk-ma
wf
,
ma-state
wf
,
top
wf
,
fpf-empty
wf
,
IdLnk
wf
,
fpf-single
wf
,
Knd
wf
,
Id
wf
origin
x:Id, L:(Knd List). only members of L read x 
MsgA x:Id, L:(Knd List). only members of L read x MsgA T
x.A(x)x:A. B(x)
x. t(x)
B(x)
B(x)